This invention relates to a method of analyzing a circuit having at least one structural loop within a single channel connected component within the circuit, especially, though not exclusively, for use in Computer-Aided Design (CAD) tools for Electronic Design Automation (EDA), and more particularly for deriving equivalent behavior of mixed (gate and switch) level digital circuits.
Contemporary chip design depends critically on the availability of appropriate EDA CAD tools in order to keep up with the ever-increasing chip complexity. Designers typically work with chip descriptions at several levels of abstraction. The Register-Transfer Level (RTL) describes a circuit at the high level of boolean functions and data flow within the circuit much like a regular programming language does. Gate-level descriptions provide a structural (schematic) description of a circuit as an interconnection of basic blocks called gates, whereas every gate has a known and relatively simple boolean behavior. Switch-level descriptions represent the lowest level of circuit design abstraction which again is a structural (schematic) one and contains an interconnection of switches (transistors) that implement the desired functionality of the circuit.
RTL is often the preferred abstraction level for most design activities. However, any RTL design has to be translated into an equivalent switch-level design as a necessary step prior to the fabrication of the chip. This translation can be performed using so-called synthesis EDA tools that compile RTL designs into a predefined, technology-specific gate-level cell library that contains a switch-level schematic for each cell. In some cases, especially when a chip has to meet stringent operating requirements (speed, power consumption, etc.), certain blocks of the chip may be designed at the switch level.
For a number of reasons, it is highly desirable and advantageous to accurately translate the functionality implemented by a circuit description containing switches into a higher level (gate or RTL) one. A very important application of such a technology is formal functional verification of circuits. Formal functional verification aims to ensure that a chip operates as expected based on appropriate mathematical models. Unlike traditional functional verification approaches, such as simulation, formal verification provides 100% coverage of a circuit""s functionality. To enable formal functional verification at the mixed (switch and gate) level, a method is required to translate the structural description of a circuit into a functional (Boolean) description in the corresponding mathematical model. Other application areas for mixed (switch and gate) level circuit analysis and translation include technology-specific library characterization, Automatic Test Pattern Generation (ATPG), and re-synthesis and re-design of chips from one chip manufacturing technology to another.
Various techniques have been developed for the analysis of the behavior of mixed (switch and gate) level circuits. These techniques process the circuit in parts called Channel Connected Components (CCC). A CCC comprises transistors that are electrically connected to each other via their channel terminals and other transistors in the CCC, and gates connected to the channel terminals of any transistor in the CCC. The CCCs in a circuit can be analyzed one at a time; individual CCC behavior is then composed to obtain the behavior of the complete circuit.
A key aspect in deriving a functional model of a single CCC is the ability to identify and properly characterize the behavior introduced by structural dependency loops within CCCs in the circuit. A structural loop within a CCC occurs when one or more transistors and/or one or more gates in the CCC is/are controlled by one or more nets that are also within that CCC. Such nets are referred to as internal inputs of the CCC, in contrast to the external inputs of the CCC, which are outputs of other CCCs and thus do not belong to the CCC. Structural loops within a CCC may result in combinational, sequential, or oscillatory behavior.
Existing approaches resolve internal inputs by either introducing a potentially large number of nets in an unknown state, or completely ignore the problem. For example, the ANAMOS and TRANALYZE tools, as presented in the article xe2x80x9cBoolean Analysis of MOS Circuitsxe2x80x9d by R. E. Bryant published in IEEE TCAD, 6(4), pp. 634-649, July 1987, and later refined in the article xe2x80x9cExtraction of Gate-Level Models from Transistor Circuits by Four-Valued Symbolic Analysisxe2x80x9d also by R. E. Bryant and published in ICCAD ""91 form and then solve a system of Boolean equations for each CCC. This works well when the system has a unique solution, but results in many unknown net values otherwise. The ANAMOS and TRANALYZE tools were developed at the Carnegie Mellon University for the purpose of transistor-level simulation and mapping into a hardware-based gate-level simulator and cannot properly analyze designs which contain sequential behavior in a single CCC. This essentially prohibits the interaction of ANAMOS and TRANALYZE with the majority of the currently available EDA CAD tools.
Another approach to mixed (gate and switch) level circuit analysis has been implemented in the Verity tool developed by International Business Machines Corporation, and described in the article xe2x80x9cVerityxe2x80x94a Formal Verification Program for Custom CMOS Circuitsxe2x80x9d by A. Kuehlmann, A. Srinivasan and D. P. LaPotin published in the IBM R and D Journal, Vol. 39, pp. 149-165, January-March 1995. This tool is a logic checker working at the switch level. The tool does not output an equivalent higher-level model nor does it work directly on sequential designs.
The present invention therefore seeks to provide a method of analyzing a circuit having at least one structural loop within a channel connected component, which overcomes, or at least reduces the above-mentioned problems of the prior art.
Accordingly, the invention provides a method of analyzing a circuit; the circuit having at least one structural loop within a channel connected component, the method comprising the steps of:
at least partly notionally splitting the circuit into its constituent channel connected components;
detecting at least one structural loop within a channel connected component;
inserting a pair of temporary Boolean variables at a break point in the at least one structural loop at an internal input within the channel connected component;
repeating the step of inserting a pair of temporary Boolean variables for each detected structural loop within the channel connected component;
analyzing the channel connected component utilizing the pairs of temporary boolean variables at the break points in order to obtain a pair of Boolean equations at each break point representing the functionality of the channel connected component at that break point to produce a system of Boolean equations for the break points within the channel connected component; and
solving the system of Boolean equations to produce a result that indicates whether the channel connected component has oscillatory, combinational or sequential behavior.
The result produced in the step of solving the system of Boolean equations can, conveniently, depend on the number of solutions that the system of Boolean equations has.
Preferably, a result that indicates that the system of Boolean equations has no solutions represents oscillatory behavior in the channel connected component, a result that indicates that the system of Boolean equations has a single solution represents combinational behavior in the channel connected component and a result that indicates that the system of Boolean equations has more than one solution represents sequential behavior in the channel connected component.
When the result indicates that the system of Boolean equations has no solutions, the method preferably further comprises the step of outputting a signal indicating that the channel connected component exhibits oscillatory behavior.
When the result indicates that the system of Boolean equations has a single solution, the method preferably further comprises the step of utilizing the single solution to produce an RTL representation of the channel connected component in any desired RTL language.
When the result indicates that the system of Boolean equations has more than one solution, the method preferably further comprises the steps of:
determining which internal inputs are coupled solely to data storage elements in the channel connected component and which internal inputs are at least partly dependent on external inputs to the channel connected component;
replacing the temporary Boolean variables by predetermined parameters at the break point in the at least one structural loop at each internal input which is coupled solely to data storage elements in the channel connected component; and
resolving the system of Boolean equations using the predetermined parameters in place of the temporary Boolean variables that were replaced to produce a pair of Boolean functions for each of the internal inputs that are at least partly dependent on an external input.
In a preferred embodiment, the pairs of Boolean functions are utilized to produce an RTL representation of the channel-connected component in any desired RTL language.